(0) Obligation:
JBC Problem based on JBC Program:
Manifest-Version: 1.0
Created-By: 1.6.0_24 (Apple Inc.)
Main-Class: NO_11
public class NO_11 {
public static void main(String args[]) {
int j = 100;
for (int i = 0; i < j; i++) {
if (i < j - 2) continue;
if (i > j - 2) break;
j++;
}
}
}
(1) JBCNonTerm (EQUIVALENT transformation)
Reached a loop using the following run:
0:
<NO_11.main||0: push 100|| - || ->
String.serialVersionUID: -6849794470754667710L
String.serialPersistentFields: a1000446
String.CASE_INSENSITIVE_ORDER: o500224
String$CaseInsensitiveComparator.serialVersionUID: 8575799808933029326L
RuntimeException.serialVersionUID: -7034897190745766939L
Exception.serialVersionUID: -3387516993124229948L
Throwable.serialVersionUID: -3042686055658047285L
o500224!: String$CaseInsensitiveComparator()
a1000446([java.io.ObjectStreamField|]): length 0
a1000448([java.lang.String...]): length [0,+inf)
1:
<NO_11.main||2: store INT to #1|| - ||100>
String.serialVersionUID: -6849794470754667710L
String.serialPersistentFields: a1000446
String.CASE_INSENSITIVE_ORDER: o500224
String$CaseInsensitiveComparator.serialVersionUID: 8575799808933029326L
RuntimeException.serialVersionUID: -7034897190745766939L
Exception.serialVersionUID: -3387516993124229948L
Throwable.serialVersionUID: -3042686055658047285L
o500224!: String$CaseInsensitiveComparator()
a1000446([java.io.ObjectStreamField|]): length 0
a1000448([java.lang.String...]): length [0,+inf)
2:
<NO_11.main||3: push 0||#1: 100|| ->
String.serialVersionUID: -6849794470754667710L
String.serialPersistentFields: a1000446
String.CASE_INSENSITIVE_ORDER: o500224
String$CaseInsensitiveComparator.serialVersionUID: 8575799808933029326L
RuntimeException.serialVersionUID: -7034897190745766939L
Exception.serialVersionUID: -3387516993124229948L
Throwable.serialVersionUID: -3042686055658047285L
o500224!: String$CaseInsensitiveComparator()
a1000446([java.io.ObjectStreamField|]): length 0
a1000448([java.lang.String...]): length [0,+inf)
3:
<NO_11.main||4: store INT to #2||#1: 100||0>
String.serialVersionUID: -6849794470754667710L
String.serialPersistentFields: a1000446
String.CASE_INSENSITIVE_ORDER: o500224
String$CaseInsensitiveComparator.serialVersionUID: 8575799808933029326L
RuntimeException.serialVersionUID: -7034897190745766939L
Exception.serialVersionUID: -3387516993124229948L
Throwable.serialVersionUID: -3042686055658047285L
o500224!: String$CaseInsensitiveComparator()
a1000446([java.io.ObjectStreamField|]): length 0
a1000448([java.lang.String...]): length [0,+inf)
4:
<NO_11.main||5: load INT #2||#1: 100, #2: 0|| ->
String.serialVersionUID: -6849794470754667710L
String.serialPersistentFields: a1000446
String.CASE_INSENSITIVE_ORDER: o500224
String$CaseInsensitiveComparator.serialVersionUID: 8575799808933029326L
RuntimeException.serialVersionUID: -7034897190745766939L
Exception.serialVersionUID: -3387516993124229948L
Throwable.serialVersionUID: -3042686055658047285L
o500224!: String$CaseInsensitiveComparator()
a1000446([java.io.ObjectStreamField|]): length 0
a1000448([java.lang.String...]): length [0,+inf)
In the loop head node, references [i193, i192] were interesting.
By SMT, we could prove
((100 <= initial_i192 and 0 <= initial_i1) and ((((path1_i196 = (path1_i192 - 2) and path1_i197 = (path1_i193 + 1) and path1_i192 = res_i192 and path1_i197 = res_i193 and path1_i1 = res_i1 and path1_i192 = initial_i192 and path1_i193 = initial_i193 and path1_i1 = initial_i1) and (path1_i193 < path1_i192 and path1_i193 < path1_i196)) or ((path2_i196 = (path2_i192 - 2) and path2_i199 = (path2_i192 - 2) and path2_i258 = (path2_i192 + 1) and path2_i259 = (path2_i193 + 1) and path2_i258 = res_i192 and path2_i259 = res_i193 and path2_i1 = res_i1 and path2_i192 = initial_i192 and path2_i193 = initial_i193 and path2_i1 = initial_i1) and (path2_i193 < path2_i192 and path2_i193 >= path2_i196 and path2_i193 <= path2_i199))) and (((res_i196 = (res_i192 - 2) and res_i197 = (res_i193 + 1)) and !(res_i193 < res_i192 and res_i193 < res_i196)) and ((res_i196 = (res_i192 - 2) and res_i199 = (res_i192 - 2) and res_i258 = (res_i192 + 1) and res_i259 = (res_i193 + 1)) and !(res_i193 < res_i192 and res_i193 >= res_i196 and res_i193 <= res_i199)))))
to be UNSAT. Consequently, the loop will not terminate.